Search for: All records

Ensuring the proper use of sensitive data in analytics under complex privacy policies is an increasingly critical challenge. Many existing approaches lack portability, verifiability, and scalability across diverse data processing frameworks. We introduce PICACHV, a novel security monitor that automatically enforces data use policies. It works on relational algebra as an abstraction for program semantics, enabling policy enforcement on query plans generated by programs during execution. This approach simplifies analysis across diverse analytical operations and supports various front-end query languages. By formalizing both data use policies and relational algebra semantics in Coq, we prove that PICACHV correctly enforces policies. PICACHV also leverages Trusted Execution Environments (TEEs) to enhance trust in runtime, providing provable policy compliance to stakeholders that the analytical tasks comply with their data use policies. We integrated PICACHV into Polars, a state-of-the-art data analytics framework, and evaluate its performance using the TPC-H benchmark. We also apply our approach to real-world use cases. Our work demonstrates the practical application of formal methods in securing data analytics, addressing key challenges. 

Ice-nucleating proteins (INPs) catalyze ice formation at high subzero temperatures, with major biological and environmental implications. While bacterial INPs have been structurally characterized, their counterparts in other organisms remain unknown. Here, we identify a new class of efficient INPs in fungi. These proteins are membrane-free, adopt β-solenoid folds, and multimerize to form large ice-binding surfaces, showing mechanistic parallels with bacterial INPs. Structural modeling, sequence analysis, and functional assays show they are encoded by orthologs of the bacterial InaZ gene, likely acquired via horizontal gene transfer. Our results demonstrate that distinct lineages have independently converged on a common molecular strategy to overcome the energetic barriers of ice formation. The discovery of cell-free INPs provides tools for freezing applications and reveals biophysical constraints on nucleation across life. 

Model predictive control (MPC) has been applied to many platforms in robotics and autonomous systems for its capability to predict a system’s future behavior while incorporating constraints that a system may have. To enhance the performance of a system with an MPC controller, one can manually tunethe MPC’s cost function. However, it can be challenging due to the possibly high dimension of the parameter space as well as the potential difference between the open-loop cost function in MPC and the overall closed-loop performance metric function. This letter presents Difffune-MPC, a novel learning method, to learn the cost function of an MPC in a closed-loop manner. The proposed framework is compatible with the scenario where the time interval for performance evaluation and MPC’s planning horizon have different lengths. We show the auxiliary problem whose solution admits the analytical gradients of MPC and discuss its variations in different MPC settings, including nonlinear MPCs that are solved using sequential quadratic programming. Simulation results demonstrate the learning capability of DiffTune-MPC and the generalization capability of the learned MPC parameters.